perm filename PROVER.DOC[P,JRA]6 blob
sn#062830 filedate 1973-09-20 generic text, type T, neo UTF8
STANFORD ARTIFICIAL INTELLIGENCE PROJECT SEPTEMBER 1973
OPERATING NOTE 73
PRELIMINARY USER'S MANUAL
FOR
INTERACTIVE THEOREM PROVER
BY
JOHN ALLEN
ABSTRACT:
This document represents a short guide to using a development of the
program originally described in Allen and Luckham [MI5]. Many of the
later sections, on pattern matching and subroutining especially, are
still in a rudimentary stage of development. Experiments
demonstrating various applications of the strategies and the user
oriented features are described in a forthcoming report,
"Applications of First Order Proof Procedures" by Allen, Luckham, and
Morales.
SAILON-73 Preliminary User's Manual
TABLE OF CONTENTS
Section 1. Introduction..................................... 2
1-I EXAMPLES.................................... 2
1-II GETTING ALONG WITH THE SYSTEM...............15
Section 2. Bookeeping and Editing Commands..................16
2-I GENERAL BOOKEEPING COMMANDS.................17
2-II COMMANDS TO EXAMINE THE LIST OF CLAUSES.....19
2-III COMMANDS TO NAME CLAUSES....................21
2-IV SEARCHING AND PATTERN MATCHING..............24
2-V PRIMITIVE PATTERN LANGUAGE..................25
Section 3. Guiding the proof................................27
3-I COMMANDS FOR PERFORMING RULES OF INFERENCE..27
3-II COMMANDS FOR SUB-PROOFS.....................29
3-III COMMANDS USEFUL WHEN NO PROOF IS FOUND......32
Section 4. The language of strategies.......................33
4-I CHOICE STRATEGIES...........................34
4-II EDITING STRATEGIES..........................37
4-III COMBINING PRIMITIVE STRATEGIES..............38
4-IV AUTOMATIC STRATEGY SELECTION................39
Section 5. Theorem proving primitives.......................40
Section 6. The answer extractor.............................43
Appendix. The BNF equations for the prover..................45
A-I THE INPUT FORMAT............................45
A-II THE STRATEGY LANGUAGE.......................47
A-III THE COMMAND LANGUAGE........................48
A-IV THE MATCHER.................................50
1
SAILON-73 Preliminary User's Manual
Section 1. Introduction.
1-I. EXAMPLES
Perhaps the easiest introduction is to follow the development of a
few examples.
Example 1.
Consider the following simple problem from propositional calculus:
Given A(a) ⊃ B, and ¬A(a) ⊃ B, prove B.
This problem could be presented to the prover as:
PRE_PRED: A,B;
PRE_OP: a;
HYPS: A(a)⊃B;
¬A(a)⊃B;
THM: B;
;
Or perhaps in a less trivial vein:
Example 2.
Consider the following set of statements:
(1) (∀x∀y)(P(x,y) ∧ P(y,z) ⊃ G(x,z))
(2) (∀y∃x)(P(x,y))
We might interpret these statements as claiming
"For all x and y, if x is the parent of y and y is the parent
of z, then x is the grandparent of z,"
and
"Everyone has a parent."
Given these statements as hypotheses we might wish to know if there
were individuals, x and y such that x is the grandparent of y. We
could pose that question as the statement:
(3) (∃x∃y){G(x,y)}
It is clear that (3) does indeed follow from (1) and (2). How do we
formulate the problem for the theorem prover?
2
SAILON-73 Preliminary User's Manual
Here is one axiomatization:
PRE_PRED: P,G;
VAR:x,y,z;
G1: ∀(x,y)(P(x,y) ∧ P(y,z) ⊃ G(x,z));
G2: ∀y∃x P(x,y);
THM: ∃(x,y)G(x,y);
;
Some of the conventions displayed in the examples are:
(1) the predicate letters and function symbols must be declared
according to their type. For example infix and prefix operators are
declared by INF_OP and PRE_OP respectively. Constants should be
declared as PRE_OPs. Similarly infix and prefix predicate symbols
must be declared as INF_PRED and PRE_PRED respectively. Propositional
letters should be declared to be prefix predicate symbols.
(2) variables must be declared; the effect of the variable
declaration is to declare the identifier as a variable prefix. The
set of variables is automatically augmented to include 9 additional
`subscripted' variants of each declared variable. For example, if x
is declared as a variable then x1,x2,..,x9, are also variables and
need not be declared.
(3) each statement must be terminated with a semicolon.
(4) statements or sets of statements may be labeled. These labels
can be used to refer to clauses in the on-line editor. If a
statement is labeled, THM, then the negation of that statement is
formed and is used in the list of input statements.
(5) adjacent like quantifiers may combined.
3
SAILON-73 Preliminary User's Manual
(6) the whole set of declarations and input statements must be
delimited by a semicolon.
A complete description of the syntax and semantics of the input
format is given in the Appendix.
4
SAILON-73 Preliminary User's Manual
Example 3.
In an investigation of axiomatizations of elementary group theory the
following statements arose:
(1) x*x = y*y
(2) x*(y*y) = x
(3) x*(y*z) = z*(y*x)
(4) x*(x*y) = y
(5) (x*z)*(y*z) = x*y
Question: Does (5) follow from (1)-(4)?
The answer is "yes" but it is not immediately obvious. It is more
difficult to establish than Example 2. Notice that this example is a
pure equality formulation (i.e., equality is the only predicate so
that all formulas are in fact equations). This example could be
presented to the prover as:
INF_OP: *;
INF_PRED: =;EQUALITY:=;
VAR: x,y,z;
AXIOMS: x*x = y*y;
x*(y*y) = x;
x*(y*z) = z*(y*x);
x*(x*y) = y;
THM:(x*z)*(y*z) = x*y;
;
In this example, the name AXIOMS refers the first four statements.
Before presenting a more complicated example, we shall describe how
to use the prover on these first Examples.
5
SAILON-73 Preliminary User's Manual
Once the input file has been prepared you are ready to used the
theorem prover. The command: RUN PROVER [P,JRA], will select the
current version of the program. The appearance of an asterisk (*)
signifies that the program is ready. If you wish the program to make
an initial selection of strategies for your problem then type:
(PROVE DSK: filename). The exact strategies which are chosen are
described in Section 4. If you would rather select you own
strategies then type: (TRY DSK: filename). You will then be asked to
describe your choice and editing strategies. See Section 4 for a
complete description of strategy selection.
If the (translations of) the set of input statements are found to be
inconsistent, then the sequence of deductions which exhibits that
inconsistency is displayed on the console. This refutation and the
set of strategies which were employed are also saved on a disk file .
The name of the file is created from the name of the input file.
Thus, for example, (PROVE DSK: FOO) or (PROVE DSK: (FOO.A)) would
create an output file named N1FOO.PRF. If the input initially comes
for the console using (PROVE) or (TRY), then the output file is given
the name, N1PRF.PRF.
It is also possible that the prover terminates without finding a
refutation. This could occur either because the selected strategies
do not form a complete set or because the initial set of clauses is
not inconsistent. In either case the program types NO-PROOF-FOUND and
enters the clause editor to wait for commands from the user.
6
SAILON-73 Preliminary User's Manual
See Section 2 for a description of the the online commands.
7
SAILON-73 Preliminary User's Manual
The first example is so simple that we shall just type it in on-
line. The output will then be found on the file N1PRF.PRF. Material
preceeded by | is commentary; statements typed by the user are
preceeded by *.
*RU PROVER [P,JRA] |retrieve the prover.
*(PROVE) |The prover is to pick strategies
*PRE_PRED:A,B; |and input is from the teletype.
PRE_PRED:A,B; |Declaration is echoed by prover.
*PRE_OP:a;
PRE_OP:a;
*HYPS: A(a)⊃B;¬A(a)⊃B;
HYPS |The statements are echoed.
A(a)⊃B;
¬A(a)⊃B;
*THM:B; |We wish to prove B.
THM
B;
*; |This final semicolon signals the end
|of the input.
HERE-ARE-THE-CLAUSES: |Here are the translations of the
|input statements.
1 A(a)⊃B;
2 B∨A(a);
3 ¬B; |Notice that the statement of the
|theorem(THM) has been negated.
4 A(a); |The first deduction.
5 ¬A(a); |Another deduction.
COUNT 3
LEVEL 1 |These are statistics printed by the
ELAPSED-TIME 134 |prover. Time is in milliseconds.
6 B;
COUNT 5
LEVEL 2 |The end of level-2 deductions.
ELAPSED-TIME 288
|A proof has been found.
|NIL is our representation for
|contradiction.
NIL 1 6 |Here's a proof-tree:
1 B; 3 4 | 6 5
3 A(a); 5 6 | \ /
4 A(a)⊃B; HYPS | 3 4
5 B∨A(a); HYPS | \ /
6 ¬B; THM | 1 6
* | \ /
| NIL
Notes:
8
SAILON-73 Preliminary User's Manual
1. Though all statements are stored internally in conjunctive
normal form, an attempt is made to improve the readibility on
output. Clauses are translated for output as follows:
a)clauses containing only positive literals appear as a
disjunction.
b)clauses containing only negative literals appear as the
negation of a conjunction.
c)mixed clauses, containing positive and negative literals
appear in the form of an implication.
9
SAILON-73 Preliminary User's Manual
Now let's try running the second example. Assume that a disk file,
EX1, has been prepared containing the axiomatization. What follows is
a running commentary on what should occur.
*RUN PROVER [P,JRA] |retrieve the current prover.
*(PROVE DSK: EX1) |Request that the program pick the
|strategies while running EX1.
PRE_PRED: P,G; |The program is accepting the axioms.
VAR: x,y,z;
G1:
∀(x,y)(P(x,y) ∧ P(y,z)) ⊃ G(x,z));
G2:
∀y∃x P(x,y);
THM:
∃(x,y)G(x,y);
HERE-ARE-THE-CLAUSES: |What follows are the translations
|of the input into clause-form.
1 P(x,z)∧P(y,z) ⊃ G(x,y) |
2 P(G21(x),x) |G21 is a generated Skolem function.
3 ¬G(x,y) |The translation of the negation of
|the theorem.
4 ¬(P(z,x)∧P(x,y)) |A deduction which has been added to
|the list of clauses.
COUNT = 1 |There was only one resolvent formed
LEVEL = 1 |on level one.
ELAPSED-TIME = 333 |The execution time in milliseconds.
5 ¬P(x,y);
COUNT = 3
LEVEL = 2 |Three resolvents have been formed by
ELAPSED-TIME = 500 |the end of level 2. (Two have been
|retained.)
NIL 1 4 |A contradiction. These next six
1 -P(x,y) 3 4 |lines are the refutation. I.e.:
3 ¬(P(z,x)∧P(x,y)) 5 6 | 6 5
4 P(G21(x),x) G2 | \ /
5 P(x,z)∧P(y,z) ⊃ G(x,y) G1 | 3 4
6 ¬G(x,y) THM | \ /
| 1 4
| \ /
| NIL
10
SAILON-73 Preliminary User's Manual
Notes:
1. A copy of the refutation tree, relevant statistics, and a
description of the actual strategies used, now appears on a
file named N1EX1.PRF.
11
SAILON-73 Preliminary User's Manual
Now let's run the third example. Assume that the axiomatization is on
a file named EX2.
*RUN PROVER [P,JRA]
*(PROVE DSK: EX2) |Again, let the program
|pick the strategies.
INF_OP: *;
INF_PRED: =;
EQUALITY: =;
VAR:x,y,z;
AXIOMS:
x*x=y*y;
x*(y*y)=x;
x*(y*z)=z*(y*x);
x*(x*y)=y;
THM:
(x*z)*(y*z)=x*y;
HERE-ARE-THE-CLAUSES:
1 x*x=y*y
2 x*(y*y)=x
3 x*(y*z)=z*(y*x)
4 x*(x*y)=y
¬(THM1*THM3)*(THM2*THM3)=THM1*THM2
|Again, THMn's are generated
|Skolem constants.
NIL 1 2 |An immediate contradiction
1 x=x; |We know E is reflexive
2 ¬THM1*THM2=THM1*THM2; 3 4 |moderate mystery.
3 x*(y*z)=z*(y*x); AXIOMS
4 ¬(THM1*THM3)*(THM2*THM3)=THM1*THM2; THM
Notes:
1. The `refutation' is a bit mysterious. A more sympathetic proof
recovery mechanism is contemplated, but perhaps some of the current
mystery can be dispelled.
A `natural' proof might be:
I. (x*z)*(y*z) = z*(y*(x*z)) replacement in THM
using CLAUSE 3.
II. z*(y*(x*z)) = z*(z*(x*y)) replacement in I
using CLAUSE 3.
III.z*(z*(x*y)) = x*y replacement in II
using CLAUSE 4 .
12
SAILON-73 Preliminary User's Manual
The above proof is indeed a translation of the machine proof. See
the proof tree below.
The proof is generated using the following rule: Besides replacement,
the prover also has a special rule of simplification. Whenever an
equality formulation is presented to the prover a list is made
consisting of all the equalities which occur in the input. In the
current example, this list would consist of everything but the
negation of the theorem. Let t1=t2 be a member of the list. Whenever
a deduction is formed (but before it has been added to the memory of
the prover) we attempt to match t1 against terms occurring in the
deduction. If matches can be made we replace those terms with the
appropriate instance of t2. It is this simplified deduction which is
presented to the editing strategies of the prover.
13
SAILON-73 Preliminary User's Manual
Thus the refutation really is:
¬(THM1*THM3)*(THM2*THM3)=THM1*THM2 THM
\
\
\ x*(y*z)=z*(y*x) AXIOMS
\ /
\ /
¬THM3*(THM2*(THM1*THM3))=THM1*THM2 by replacement
\
\
\ x*(y*z)=z*(y*x) AXIOMS
\ /
\ /
¬THM3*(THM3*(THM1*THM2))=THM1*THM2 by simplification
\
\
\ x*(x*y)=y AXIOMS
\ /
\ /
¬THM1*THM2=THM1*THM2 by simplification
\
\
\ x=x
\ /
\ /
NIL
by resolution
14
SAILON-73 Preliminary User's Manual
1-II. GETTING ALONG WITH THE SYSTEM.
1) Running the prover.
RU PROVER [P,JRA]
(PROVE | TRY <input>) <input> is either DSK: <file> or null.
2) Saving a core image.
Hit space bar and wait for response(*).
The prover responds by typing its first clause.
Now type HALT.
Response: "HALT AT USER ####".
You may now save the core image.
Typing "ST" or "RUN"-ing the saved image will
have the same effect: the prover will respond
"*" and you will be back in the on-line editor.
You may continue the proof search by typing
"CONTINUE".
3) Reallocation.
Frequently it is desirable to increase the storage areas during the
execution of the prover without having to restart the whole problem.
This can be done as follows:
Hit the space bar and wait for response.
Call the monitor.
Execute "ST 141".
Call the monitor.
Execute "CORE #".
Execute "ST".
Evaluate "(REENTER)".
The prover will now resume its computation
in the enlarged work spaces.
15
SAILON-73 Preliminary User's Manual
Section 2. Bookeeping and Editing Commands.
Most applications of the prover lie in that gray area between a quick
proof and the occurrence of NO-PROOF. That is, an application of the
prover usually generates a large number of deductions before either a
proof is found or no more deductions can be made under the current
strategy settings. It is this area which can be profitably explored
using interactive commands. If the user sees a deduction which
should lead to the desired refutation he is able to guide the
program to the explicit contradiction. If he sees a deduction which
he feels is interesting, he can explore its consequences in the set
of statements. If he feels that the strategy settings are ill-chosen
then he can abandon the current proof-search and pick new strategies.
The next sections give detailed descriptions of the current on-line
commands.
All of the commands may be abbreviated to their first two letters.
First, the on-line editor is entered by striking the space bar.
16
SAILON-73 Preliminary User's Manual
2-I. GENERAL BOOKEEPING COMMANDS.
CHange CH;
It is frequently desirable to change some of the
strategies while a proof attempt is in progress.
CHange describes what choice and editing strategies
are currently active and asks which are to be
changed. If a change is desired type YES(or Y) and
follow with the desired strategy; if no change is
needed, type NO(N).
COntinue CO;
This command is used to exit from the on-line editor
and continue the interrupted proof search.
CUrrent CU;
This command simply lists the current strategy
settings.
DSkout DS <filename>;
This command diverts future output to the specified
disk file. Use the EOf command to terminate the
DSkout command.
EVal EV;
This command is mostly a debugging aid and is
included for completeness. The casual users should
not have to resort to its use. EVal enters a READ-
EVAL-PRINT loop. To return to the editor, type @END.
HAlt HA;
HAlt stops the prover in such a state that if the
current core image is saved, it can be continued. To
resume execution of such a core image, type RUN DSK:
name. When the asterisk appears you are in the on-
line editor. Then type COntinue.
End Of file EO;
EOf is used to terminate the DSkout command.
HElp HE;
17
SAILON-73 Preliminary User's Manual
This command will type a list of the available
editing commands along with an abbreviated
description of their action.
18
SAILON-73 Preliminary User's Manual
2-II. COMMANDS TO EXAMINE THE LIST OF CLAUSES
Each clause which has been retained by the prover -- initial clause
or deduction -- is given a number, the first axiom, the number 1.,
etc.. These numbers are permanently assigned, even though certain
actions of the prover may delete clauses from active status (in
which case they are not used in making any future deductions).
Clauses which have been so deleted are displayed as *DE*. When the
editor is entered, an invisible pointer is initialized to the first
clause. This first set of commands allow the user to manipulate the
set of clauses using the pointer or the numbers associated with the
clauses.
FLoat UP FU; or FL UP;
Moves the pointer up through the clause list
displaying each clause. The motion is stopped either
by striking a key or by reaching the upper extreme of
the list. FLoat UP may also be apbbreviated as FU.
FLoat DOwn FD; or FL DO;
The counterpart of FLoat UP. FLoat Down may also be
abbreviated as FD.
UP UP n;
UP is followed by an integer, n. The effect of this
command is to move the pointer up n clauses from its
current setting. As the pointer is moved, the
interviening clauses are printed. If n = 0, then the
pointer is immediately moved to the beginning of the
clause list. As with the FLoat commands, striking a
key will stop the pointer.
DOwn DO n;
The counterpart of UP. DOwn 0 moves the pointer to
the end of the list.
19
SAILON-73 Preliminary User's Manual
GO GO n;
GO is followed by an integer designating a clause.
The pointer goes immediately to the designated
clause and the clause is printed.
20
SAILON-73 Preliminary User's Manual
2-III. COMMANDS TO NAME CLAUSES.
Though the previously described commands have proved quite useful,
experience has shown that more global manipulation of the clauses is
needed. Therefore we have developed commands for assigning names to
subsets of the clause list, and commands for manipulating these sets.
Some sets of clauses are assigned names automatically by the prover.
The main clause list is named CLAUSES; and the simplification list
for the equality rule (see Example 3, Section 1-I)is named DLIST.
Also if any of the input statements were named in the input file
those names will be present in the symbol table. Input statements
which were not named by the user can found under the name, AXIOMS.
Just as each element of the primary list of clauses is assigned a
unique positive integer, so is each element of each named subset.
For example to refer to the second element of the set named FOO, use
FOO[2]; to refer to the second and third elements, use FOO[2,3].
Clauses may thus be referenced explicitly by their number in the main
clause list or by their position in a named set.(For example, the n-
th clause is also CLAUSE[n].) Clauses may also be referenced
implicitly through the pattern matcher. See Section 2-IV.
To be more precise about the nature of clauses, the following BNF
equations will be used in the sequel:
<clauses> ::= {<c>,}*<c>
<c> ::= <number>|<id>{[{<number>,}*<number>]}*
::= @<statment>|FIND[<id>;<pattern>]|FINDC[<pattern>]
21
SAILON-73 Preliminary User's Manual
ADd ADd <clauses>;
Most of the results of the on-line commands:
deductions, insertions, substitutions, etc., are
local to the clause editor. To include any of these
resulting clauses in the memory of the prover use the
ADd command.
ANcestry AN <clauses>;
The ancestry command is used to display the
derivation tree of the specified clauses.
CLear CL <id>;
CLear takes a name as argument. This command only
removes the name from the symbol table; it does not
affect the clauses attached to the name.
Delete DE <clauses>;
The designated clauses are deleted from the memory of
the prover. Attempts to display such clauses will
print *DE*. Other attempts to use deleted clauses in
editing commands will invoke an error message.
DIsplay DI <clauses>;
This command displays all the elements of <clauses>.
SEt SE <id> <clauses>;
SEt <id> <clauses>; has the effect of assigning to
<id> the sequence of clauses selected by the
<clauses>. Within a particular proof attempt, the
names selected by the user are retained.
SUbstitute SU <term>; FOR <term>; IN <clauses>;
The effect of the SUbstitute command is to substitute
the first <term> for every occurrence of the second
<term> in copies of all of the designated <clauses>.
Notice that the original <clauses> are kept intact.
The modified <clauses> are added to the list named
ASSERT.
SYmbols SY;
22
SAILON-73 Preliminary User's Manual
Display the current symbol table of clause names.
23
SAILON-73 Preliminary User's Manual
2-IV. SEARCHING AND PATTERN MATCHING.
Pattern matching is invoked by the FIND operation.
FIND[<id>,<pattern>] expects <id> to be the name of a list of
clauses, and <pattern> should be a Boolean combination of primitive
patterns. These primitive patterns are described in the next sub-
section, but basically allow description of syntactic parts of
clauses.
Since many of the applications of FIND are of the form FIND[CLAUSES,
<pattern>], the abbreviation, FINDC[<pattern>] has been added for
this case.
Here's an example of FIND and FINDC.
SET XX FINDC[OCR[0]]; |OCR is a reserved word. The pattern says
|find all clauses in the set CLAUSES which
|have occurrences of the symbol 0.
|In this problem 0 is a function letter.
*
DI XX; |Display the clauses.
1 x/y=0 ⊃ x≤y;
2 x≤y ⊃ x/y=0;
3 0≤x;
4 x/x=0;
5 x/1=0;
*
SET YY FIND[XX,OCR[≤]]; |Find clauses in XX which have occurrences
|of the symbol '≤', and assign those clauses
|to YY.
*
DI YY; |Display YY.
1 x/y=0 ⊃ x≤y;
2 x≤y ⊃ x/y=0;
*
*
SET ZZ FIND[YY,OCR[/]∧OCR[=]];|Boolean combinations are allowed.
*
SET ZZ FIND[YY,LENGTH=1];|This command will locate all units in the
24
SAILON-73 Preliminary User's Manual
|set, YY.
2-V. PRIMITIVE PATTERN LANGUAGE.
The primitives allow description of the ancestry of a clause, the
length (number of literals) and depth (of function nesting) of
clauses, besides a very simple matching algorithm. The matcher can
match on literals , terms, predicate letters, negations of predicate
letters, or functions symbols.
PRIMITIVES:
1) primitive for ancestry: TREE[x]
"x" designates a clause. TREE[x] will match any clause whose
derivation tree contains x. N.B. the clause x itself is considered
to be derived from x.
Examples:
For example, if G1 is the name of an initial statement then :
SET YY FIND[XX,TREE[G1]]; will assign to YY all of the clauses in XX
which were derived using G1.
2) primitive for length: LENGTH
LENGTH gives the number of literals in the clauses currently being
examined. LENGTH may be tested using one of the available relations.
Examples:
LENGTH = 1 is true if the current clause is a unit.
3) primitive for depth: DEPTH
This primitive gives the depth of function nesting in the clause.
Example:
25
SAILON-73 Preliminary User's Manual
DEPTH > 4 is true if the depth of nesting in the current clause is
greater than 4.
Primitive relations:
Currently the only relations available are =, >, and <. These
relations are only to be used in comparing length and depth.
MATCHING:
4) primitive for matching: OCR
OCR is a simple matcher which expects its arguments to be a literal,
term, predicate letter, or negation of a predicate letter. OCR
matches any clause which contains a matching construct.
Variables may appear in the pattern, in which case a test for
subsumption determines when a match is to be successful.
Examples:
In the following, assume P, and = are predicate letters; assume x, y,
and z are variables; and assume a, b, c, d and f and g are function
symbols.
OCR[P] matches P(x), P(a)⊃a=b, and ¬P(b).
OCR[¬P] matches P(a)⊃a=b and ¬P(b). Note P(a)⊃a=b matches here since
the implication really is ¬P(a) ∨ a=b;
OCR[¬=]∧¬OCR[d] would match ¬f(a,b)=c but would not match ¬f(a,b)=d.
OCR[P(x)] matches P(x),¬P(g(x)) and ¬P(a).
OCR[¬P(g(x))] matches ¬P(g(a)) but not P(g(a)) or ¬P(f(g(a),x));
OCR[f(g(x),x)] matches clauses containing say, f(g(a),a) but does not
match f(g(a),b).
26
SAILON-73 Preliminary User's Manual
Section 3. Guiding the proof.
The commands listed above give us a reasonably powerful set of
instructions for manipulating the clause list. Clearly, before we can
really begin to guide the prover we must be able to perform the rules
of inference on-line. The next set of commands begins to do this.
3-I. COMMANDS FOR PERFORMING RULES OF INFERENCE
PAramodulate PA <clauses>; <clauses>;
This command handles equality replacements. All
equality literals of the form t1=t2, are used in
equality replacements in the following manner: let
t1=t2 be an equality literal occurring in a clause of
one of the <clauses>; let s be any term, not a
variable, which occurs in some literal in the other
<clauses>. If s occurs no deeper than PDEPTH (see
Section 4-I. for PDEPTH) and there is a substitution
unifying s and t1, then the occurrence of t1 is
replaced by the appropriate instantiation of t2. The
paramodulants are assigned a new name of the form
PARn. See the REsolve command.
REsolve RE <clauses>;<clauses>;
This command takes a pair of <clauses> as arguments.
The resolvents of these two sets are formed, a unique
name is generated and the resolvents are assigned to
that new name. The generated names are presently of
the form RESn, for some integer,n. The created
names, PARn and RESn are only local names, that is,
returning to the prover (via COntinue) will destroy
them. Use the ADd command to save desired
computations.
SImplify SImplify <clauses>; BY <clauses>;
This command is similar to the PA command. Here the
second set of clauses is to be a list of equality
units, again of the form t1=t2. Terms occuring in the
first set of clauses which unify with elements, t1,
are replaced by instances of t2. DDEPTH determines
the depth to which the match is attempted.
27
SAILON-73 Preliminary User's Manual
Example 4. A simple example of the use of the rules of inference.
Assume that = is the equality predicate and that we have just struck
a key on the console.
*DI 1,2,3; |Display the first three clauses
1 x≤y ⊃ x/y=0
2 ¬1/(a/b)=0
3 0≤x
*PA 1; 2; |Use replacement on 1 and 2.
THE-PROVER-RETURNS-THE-FOLLOWING-LOVELY-CLAUSES
THEY-WILL-BE-FOUND-UNDER-THE-NAME: PAR1 |PAR1 is a created name.
1 1≤a/b ⊃ 1=0
*PA 2; 3; |Try to use the replacement rule
NO-PARAMODULANTS |on clauses 2, and 3.
*RE 1; 3;
THE-PROVER-RETURNS-THE-FOLLOWING-LOVELY-CLAUSES
THEY-WILL-BE-FOUND-UNDER-THE-NAME:RES1 |RES1 is another created
|name.
1 0/x=0
*PA RES1; RES1; |Created names are legal.
THE-PROVER-RETURNS-THE-FOLLOWING-LOVELY-CLAUSES
THEY-WILL-BE-FOUND-UNDER-THE-NAME:PAR2 |PAR2 is a new name.
1 0=0 |True.
*AD PAR1[1]; |Add 1≤a/b ⊃ 1=0 to the memory
|of the prover.
28
SAILON-73 Preliminary User's Manual
3-II. COMMANDS FOR SUB-PROOFS AND PROOF-CHECKING.
Though the commands, REsolve and PAramodulate, are useful for fine
control of the prover, it is often useful to demand larger inference
steps. That is, using some of the existing clauses in memory, with
perhaps some additional assumptions, we wish the prover to attempt to
establish the validity of a first order formula. While this subproof
is under investigation the state of the main proof should be
preserved. The commands in this section are used to initiate and
control such subproofs.
ABandon AB ; or AB <clauses>;
This command is used to abandon a proof attempt,
returning the prover to the previously saved state.
If <clauses> is present, then the selected clauses
are returned and assigned to a created name.
USing US <clauses>;
The selected clauses are designated to be used in the
forthcoming subproof.
PRove PR <statement>;
The <statement> is translated and will be attached to
the name LEMMA. The negation of the statement is also
formed and will be used in the subproof. Thus both
the positive and negative translates are formed. The
positive translate is maintained for the convenience
of the user since after the lemma has been
established it should be available for further
deductions. Within the subproof the negation of the
<statement> will appear under the local name, THMS.
These last two commands --USing, and PRove -- are used to initialize
the call on the prover; USing may be omitted. There are two commands
to commence the subproof.
EXecute EX;
29
SAILON-73 Preliminary User's Manual
EXecute begins the subproof using a computed set of
stategies.
TRy TR;
TRy first enters the strategy selection dialog, then
begins the subproof with the chosen strategies.
In both cases the strategies of the subproof are completely local.
They in no way affect the strategies in the parent proof. If a key is
struck while in the subproof the editor is entered and can manipulate
the local clauselist or initiate another subproof. The Continue
command will continue the subproof, the ABandon command will return
to the previous subproof level.
30
SAILON-73 Preliminary User's Manual
Example 5. A simple example of subproof generation.
Suppose that we have struck a key during a proof-search.
*AN 10; |Display the ancestry of
P(A) 1 2 |clause no. 10.
1 P(A) ∨ P(B) AX1
2 ¬P(B) HYP1
*USING 10, @P(A) ⊃ P(B); ; |Setup the assumptions for the
|lemma.
|Use clause no. 10 in the attempt
*PROVE @P(B);;
*EX; |This initiates the subproof.
NIL 1 2
1 P(A) DEDUCT |Clause 10 becomes an "axiom"
2 ¬P(A) 3 4 |within the subproof.
3 P(A)⊃P(B) INSERT
4 ¬P(B) THM |The negation of the lemma
PROOF-FOUND-FOR-LEMMA
|We are now back in the editor
*DI 10; |Display clause no. 10.
P(A)
*DI LEMMA; |The translate of the statement
P(B) |to be PROVEed.
*USING LEMMA;
*PROVE @∃(x)P(x);; |LEMMA now becomes the translate
*EX; |this clause.
NIL 1 2
1 P(B) AX1
2 ¬P(X1) THM
PROOF-FOUND-FOR-LEMMA
*DI LEMMA; |ED1 is a ubiquitous Skolem
P(ED1) |constant.
31
SAILON-73 Preliminary User's Manual
3-II. COMMANDS USEFUL WHEN NO PROOF IS FOUND
When the prover is unable to make new deductions which satisfy the
current strategies it will report that no refutation can be found,
and will enter the on-line editor. At this time the user can examine
the list of clauses, perform rules of inference, initiate sub-proofs,
save any or all of the current deductions and begin a the proof
search again, perhaps with new strategies. The user can also force a
proof attempt to be abandoned by typing AB;. This has exactly the
same effect as if the prover could make no new deductions.
ABandon AB;
AB, typed in this context (not in a subproof)
terminates the main proof attempt, enters the on-line
editor, and waits for commands.
TErminate TE <clauses>; or TE;
If <clauses> are present then they are added to the
list of clauses named THMS. The list of initial
clauses is preserved and a new proof attempt is
begun. If the initial attempt was through PROVE then
the user is asked if he still wants automatic
strategy selection. If the initial attempt was
through TRY or the user does not wish automatic
selection, then a dialogue is begun describing the
current strategies and asking if changes are desired.
Then a new proof search is begun.
This use of AB and TE is useful for feeding `interesting' deductions
back into a proof search without having to restart the whole process.
The derivation tree of any such saved derived clause is maintained
for the proof recovery mechanisms but such clauses appear to be
`input' clauses to the rules of inference.
32
SAILON-73 Preliminary User's Manual
Section 4. The Language of the Strategies
Frequently the user of a theorem prover "knows" a lot of detail about
the problem domain being axiomatized. Much of this information
(almost by definiton) is domain-dependent and thus doesn't fit the
usual set of strategies as well as could be desired. Also much of
this information is heuristic in nature and would be difficult to
express in the form of axioms. To help with these problems we have
introduced two new ideas: (1) a language for describing strategies;
and (2) new data types added to LISP so that the user may tailor-make
his own prover.
The strategy language allows Boolean expressions over properties of
clauses. Major extensions of this idea are contemplated..
The programmable aspects allow the user to describe first order
statements, strategies and pattern matching in an intuitive notation.
With these facilities inside LISP we can write new rules of inference
and domain dependent theorem provers.
33
SAILON-73 Preliminary User's Manual
4-I. THE CHOICE STRATEGIES.
Choice strategies occur in the following context: Given two possible
candidates, C1 and C2, for the application of a binary rule of
inference I, a choice strategy will determine whether not we wish to
form I(C1,C2).
Builtin choice strategies.
a) NONE allows unrestricted applications of the rules of inference.
b) ANCESTRY implements the AFF strategy; that is, to apply I either
C1 or C2 must be an initial clauses, or, either C1 must appear in the
derivation tree of C2, or C2 must appear in the tree of C1.
c) SUPPORT designates the set-of-support strategy. This strategy
basically says that every first-level deduction must have one of its
parents in the support set. SUPPORT must be followed by an argument
list describing which statements are to be supported. The elements
of the argument list may either be clause numbers or names which the
user has associated with certain input clauses.
Example: SUPPORT[1,2,AXIOM[2],THEOREM] would put clauses numbered 1
and 2, the clause AXIOM[2], and all clauses with name, THEOREM, in
the support set.
d) VINE strategy says that either C1 or C2 must be an initial clause.
This strategy is known to be incomplete, but is useful in many cases.
e) UNIT strategy says that either C1 or C2 are singletons(unit
clauses). Again, this strategy is not complete, but is useful as a
34
SAILON-73 Preliminary User's Manual
"quick-kill" or "end-game" strategy. It is easy to show that if
there is a UNIT-refutation then there is a VINE-form refutation. It
is also easy to show that if all the initial statements are either
units(singletons) or are of the form L1∧L2∧...∧Ln ⊃ M then there is a
UNIT proof.
f) P1 is the P1-deduction of Robinson. Here it is required that
either C1 or C2 contain only positive literals. This strategy is
complete.
g) MODEL is the implementation of a very simple case of the model-
relative deduction strategy of Luckham. Model-relative deduction is
a generalization of P1 deduction and is complete. Deduction relative
to a model says that at least one of the clauses C1 or C2 be false of
the model. MODEL expects an argument list describing a binary
partition of the predicate letters appearing in the initial clauses.
In the current restricted implementation this says either C1 or C2
must have zero intersection with the two members of the partition.
For example, MODEL[;<all predicate letter occurring in problem>] is
equivalent to P1-deduction; MODEL[P,=;R] defines a partition with
positive occurrences of P and =, and negative occurrences of R.
h) DEFMODEL can be used to designate a LISP function to define a
model for the current set of statements. DEFMODEL expects a single
argument which is the name of a LISP function(of one argument) and
which implements the defining conditions of a model. The use of this
strategy requires knowledge of the representation of clauses.
35
SAILON-73 Preliminary User's Manual
i) EQUALITY signals that the replacement rule, paramodulation, is to
be used. EQUALITY needs two arguments: a predicate name to be
interpreted as equality; and second, a number, called PDEPTH, which
determines how deep in the nesting of function symbols the matcher
will look in attempting to match terms. For example, a PDEPTH of 1
says only examine primary occurrences of terms.
36
SAILON-73 Preliminary User's Manual
4-II. EDITING STRATEGIES.
Editing strategies are applied to the results of the rules of
inference. These strategies are used to filter out some of the
deductions which a rule of inference has generated.
Builtin editing strategies.
a) DEMOD is a rule of simplification most commonly used in
conjunction with EQUALITY. DEMOD takes two arguments. The first
describes a list of equality units; the second, a number named DDEPTH
which,like PDEPTH, determines a bound on the matching routines.
b) DEPTH takes a single integer argument interpreted to be a bound on
the depth of function symbol nesting which must not be exceeded if
the deduction is to be retained.
For example, DEPTH[4].
c) LENGTH also takes an integer argument and gives a bound on the
number of literals which will be allowed in any deduction.
d) SELDEPTH takes function symbol-number pairs as arguments.
SELDEPTH is a refinement of DEPTH in that the allowable depth of
nesting of each function symbol is determined by the corresponding
number.
e) Any of the primitive constructs of the pattern language: TREE,
LENGTH, DEPTH, or OCR. For example if OCR[f(e,e)] were to appear in
an editing strategy then any clauses which contained "f(e,e)" would
be rejected.
37
SAILON-73 Preliminary User's Manual
4-III. COMBINING PRIMITIVE STRATEGIES.
Boolean combinations of built-in or user-defined strategies are
allowed. For example, a reasonable choice strategy is: ancestry
filter form with a set of support being the negation of the statement
to be proved. This can be written as:
ANCESTRY ∧ SUPPORT[THM];
An editing strategy which filters out all clauses whose length
(number of literals) is greater than 4 or whose depth (depth of
nesting of function symbols) is greater than 3 can be expressed as:
LENGTH[4] ∨ DEPTH [3];
See the Appendix (A-II) for the rules of combination.
38
SAILON-73 Preliminary User's Manual
4-IV. THE AUTOMATIC STRATEGY SELECTION.
A very simple procedure is used to select the strategies in PROVE-
mode. The choice strategies are ANCESTRY and, if THM is present as
an axiom name , then SUPPORT[THM] is also used. Also, if an equality
predicate letter is declared, then equality replacement with a depth
bound of 4 is added.
The editing strategies are determined by the maximum lengths and
depths which occur in the input clauses. If equality is present then
a simplification list consisting of all the positive units is used.
The strategy settings are automatically changed if the program is
terminated without finding a proof.
39
SAILON-73 Preliminary User's Manual
Section 5. Theorem proving primitives.
It is now possible to write LISP-like programs which control the
actions of the theorem prover and manipulate clauses. Data types
for CLAUSES, STRATEGIES, and PATTERNS have been added to LISP so that
the user can describe his clause manipulations in the same notation
which is used to drive the on-line prover. LISP functions, TRYTIL
and FIND, have been defined to perform controlled proof-attempts and
clause-list searching.
1. Data Types.
a) [CLAUSES <clauses>] is used to introduce new clause lists to the
program. For example: (SETQ X [CLAUSES DSK:FOO]) when executed will
assign to X the clauselist manufactured from the statements on file
FOO.
b) [CHOICE <strategy>] and [EDIT <strategy>] introduce the
appropriate strategies.
c) [PATTERN <pattern>] is useful in conjunction with FIND to filter
out clauses which match <pattern>.
2. Procedures.
(TRYTIL <clauses><choice-strategy><edit-strategy><termination
condition>)
where:
1) <clauses> is a list of clauses .
2) <choice-strategy> is a representation of a choice strategy.
3) <edit-strategy> represents an editing strategy.
40
SAILON-73 Preliminary User's Manual
4) <termination condition> is a functional argument which will be
evaluated periodically during the execution of the TRYTIL. As long
as the condition evaluated to NIL the proof attempt will continue. If
the condition becomes true then TRYTIL will return the list of all
deductions which have been made.
For example:
(TRYTIL [CLAUSES DSK: FOO] [CHOICE ANCESTRY∧SUPPORT[THM]] [EDIT
LENGTH[4]∨DEPTH[3]] (FUNCTION (LAMBDA()(GREATERP LEVEL 3))) )
will begin a proof search using file DSK:FOO with choice strategy
being AFF and supporting the negation of the theorem. Deductions
whose length is greater than 4 or whose depth of function nesting is
greater than 3 will be discarded. The proof search will terminate at
the end of level 3.
If a refutation is discovered during any attempt, (QED) is returned.
If no refutation is found, then the on-line editor is called to give
the user a chance to examine the current proof environment. There is
a third way to exit TRYTIL: since the on-line editor is available
inside the proof attempt, typing ABandon <clauses> to the editor
will force termination of the proof attempt and will return the
selected <clauses>.
(FIND <clauses><pattern>)
where: 1) <clauses> is a list of clauses. 2) <pattern> is a
condition which is to be applied to each element of <clauses>.
41
SAILON-73 Preliminary User's Manual
The value of FIND is a list of all elements of <clauses> which
satisfy the <pattern>.
42
SAILON-73 Preliminary User's Manual
Section 6. The Answer Extractor.
A subset of the Luckham-Nilsson answer-extraction algorithm has been
implemented. It is not available as part of the basic prover, but
must be loaded by the user. The prover should be run in slightly
more core to accommodate the answer routines.
Here is an example:
Recall example 2. in the introduction:
(1) ∀(x,y)P(x,y)∧P(y,z)⊃G(x,z)
(2) ∀y∃xP(x,y)
Question:(3) ∃(x,y)G(x,y) .
From the semantics of the problem we know that the "answer" to (3) is
"yes" and in fact we can display specific solutions to the problem:
The parent of the parent is the grandparent. What does the answer
extractor do with this problem?
RU DSK PROVER[P,JRA] ;get the prover
(DSKIN (P,JRA) ANSWER) ;load in answer extractor
(PROVE DSK: EX1)
...
[output as before]
...
*(ANSPRED) ;this calls the extractor
*G(G21(G21(x)),x) ;the answer
*
We must now interpret the Skolem function G21. G21 was introduced in
the translation of (2), that is, G21(y) is an object such that
P(G21(y),y). Thus G21 is a function to select the parent of an
individual. In this light our answer, G(G21(G21(x)),x), is the
expected result.
The current implementation of the answer extractor does not
43
SAILON-73 Preliminary User's Manual
recognize applications of the equality rule and will fail to get
answers in this case. It is trivial to extend the algorithm and its
implementation will occur shortly.
44
SAILON-73 Preliminary User's Manual
Appendix. The Syntax Equations for the Theorem Prover.
The parsers for the input syntax and the command language are both
contstructed by Lynn Quam's Syntax Directed Input Output program.
A-I. THE INPUT FORMAT
The usual form for input consists of the declarations of the non-
logical constituents of the axioms, followed by a sequence of
statements. The statements may be assigned names, and if a statement
whose name is the same as the current value of THEOREMNAME is present
that statement is negated before being added to the memory of the
prover. The LISP atom THEOREMNAME is initialized to THM.
<INPUT> ::=<DECOP>:<OPLIST>;
::=<ID>:
::=<STATEMENT>
<DECOP> ::=VAR | INF_OP | INF_PRED | PRE_OP | PRE_PRED | EQUALITY
<OPLIST>::=<OP>,<OPLIST>
::=<OP>
<STATEMENT> ::=;
::=<S1>;
<S1> ::=<S2>
::=<S1><EQUIV><S2>
<S2> ::=<S3>
::=<S2><IMP><S3>
<S3> ::=<S4>
::=<S3><OR><S4>
<S4> ::=<S5>
::=<S4><AND><S5>
<S5> ::=(<S1>)
::=<NOT><S5>
::=<QFF><BODY>
::=<PRED>
45
SAILON-73 Preliminary User's Manual
<BODY> ::= <IVAR><S5>
::=(<VARLIST>)<S5>
<VARLIST>::=<IVAR>,<VARLIST>
::=<IVAR>
In the following, the routines corresponding to <PREPREDLET>,
<INFPREDLET>, <IVAR>, <PREFN>, and <INFN> check the lists of prefix-
and infix- predicate and function letters, and the variable list, all
of which were manufactured by the appropriate declarations.
<PRED> ::=<PREPREDLET><ITMLST>
::=<PREPREDLET>
::=<TM><INFPREDLET><TM>
<ITMLST>::=(<ITMS>)
<ITMS> ::=<TM>,<ITMS>
::=<TM>
<TM> ::=<IVAR>
::=<PREFN><ITMLST>
::=<PREFN>
::=(<TM>)
::=<TM><INFN><TM>
The logical connectives are defined as follows:
<EQUIV> ::= ≡ | ↔
<IMP> ::= ⊃
<OR> ::= ∨
<AND> ::= ∧
<NOT> ::= ¬
<QFF> ::= ∀ | ∃
46
SAILON-73 Preliminary User's Manual
A-II. THE SIMPLE STRATEGY LANGUAGE
The most straightforward application of the strategy language
consists of using Boolean combinations of the builtin strategies.
<STRATEGY>::=<F1>;
<F1> ::=<F2>
::=<F1><OR><F2>
<F2> ::=<F3>
::=<F2><AND><F3>
<F3> ::=(<F1>)
::=<NOT><F3>
::=<PREDIC>
<PREDIC>::=ANCESTRY
::=NONE
::=VINE
::=UNIT
::=P1
::=SUPPORT[<C>]
::=MODEL[<PREDLST>;<PREDLST>]
::=EQUALITY[<OP>;<NUMBER>]
::=DEMOD[<CLAUSES><NUMBER>]
::=DEFMODEL[ID]
::=LENGTH[<NUMBER>]
::=DEPTH[<NUMBER>]
::=SELDEPTH[<FNLST>]
::=<MPRM>
<PREDLST>
::=<ID>,<PREDLST>
::=<ID>
::=
<FNLST> ::= <FP>;<FNLST>
::= <FP>
<FP> ::=<OP>,<NUMBER>
47
SAILON-73 Preliminary User's Manual
A-III. THE COMMAND LANGUAGE
<CLAUSES> ::= <C>,<CLAUSES>
::= <C>
<C> ::= @<STATEMENT> <STATEMENT> is in A-I.
::= DSK: <FILE>
::= <NUMBER>
::= <ID>[<VARLIST>]
::= <ID>
::= FIND [<ID>,<MATCH>]
::= FINDC [<MATCH>]
<FILE> ::= <ID>
::= (<ID>.<ID>)
<VARLIST> ::= <NUMBER>,<VARLIST>
::= <NUMBER>
<COMMAND ::= AB <CLAUSES>; ABandon proof attempt
::= AB;
::= AD <CLAUSES>; ADd clauses to clauselist.
::= AN <CLAUSES>; display ANcestry
::= CH; CHange strategies
::= CL <ID>; CLear name from symbol table
::= CO; COntinue with proof search
::= CU; display CUrrent strategies
::= DE <CLAUSES>; DElete clauses
::= DI <CLAUSES>; DIsplay clauses
::= DO <NUMBER>; move DOwn
::= DS <FILE>; set output to DSk(see EOf)
::= EO; make End Of File
::= EV; enter Lisp's EVAL
(leave via @END)
::= EX; EXecute subproof with
standard strategies.
::= FD; Float Down clause list
::= FU; Float Up clause list
::= GO <NUMBER>; GO to designated clause
::= HA; HAlt to prover
::= HE; type HElp message
48
SAILON-73 Preliminary User's Manual
::= PA <CLAUSES>;CLAUSES>; PAramodulate selected
clauses.
::= PR <CLAUSES>; Initialize subproof
(see US,EX,and TR.)
::= RE <CLAUSES>;<CLAUSES>; REsolve clauses
::= SE <ID> <CLAUSES>; SEt id as name for clauses.
::= SI <CLAUSES>; BY <CLAUSES>; SImplify
::= SU <TM> FOR <TM> IN <CLAUSES>; SUbstitute.
(add to ASSERT)
::= SY; display current SYmbol table.
::= TE <CLAUSES>; TErminate; (see Sec. 2-IV).
::= TE;
::= TR; TRies subproof with user's
strategies.
::= UP <NUMBER>; move UP n clauses.
49
SAILON-73 Preliminary User's Manual
A-IV. THE MATCHER
<MATCH> ::= <M2>
::=<MATCH> ∨ <M2>
<M2> ::= <M3>
::= <M2> ∧ <M3>
<M3> ::= (<F1>) <F1> in A-II.
::=¬<M3>
::=<MPRM>
<MPRM> ::= <ARG><MOP><ARG1>
::= OCR[<PAT>]
::=TREE[<CNAME>]
<MOP> ::= =
::= <
::= >
<ARG1> ::= <ARG>
<ARG> ::= LENGTH
::=DEPTH
::=<NUMBER>
<CNAME> ::= <NUMBER>
::= <ID>[<VARLIST>] <VARLIST> in A-III.
::= <ID>
<PAT> ::= <NOT><PRED> <PRED> in A-I.
::=<PRED>
::=<TM> <TM> in A-I.
::=<FNLET>
<FNLET> ::=<INFN> <INFN> in A-I.
::=<PREFN> <PREFN> in A-I.
50